$\vdash$  $\forall$$T$:Type, $L$:($T$ List). ($\neg$($\uparrow$null($L$))) $\Rightarrow$ (hd($L$) $\in$ $L$)